$LOAD_PATH.unshift File.join(File.dirname(__FILE__),'../..','ext_pr1/lib')
require 'ext_pr1_v4'

#definieren der nötigen Konstanten:
#sekunden pro minute = 60, minuten pro stunde = 60, Stunden pro Tag = 24
#stunde in sekunden = sekunden pro minute * minuten pro stunde
#tag in sekunden = stunde in sekunden * stunden pro tag

MIN_IN_SEC = 60
HOUR_IN_MIN = 60
DAY_IN_HOUR = 24
HALF_DAY_IN_HOUR = DAY_IN_HOUR/2

HOUR_IN_SEC = MIN_IN_SEC * HOUR_IN_MIN
DAY_IN_SEC = DAY_IN_HOUR * HOUR_IN_SEC
HALF_DAY_IN_SEC = DAY_IN_SEC/2
#arithmetik einer uhr, die mit beliebigen zuständen arbeiten kann

  def halve?(param) param.symbol? and param.in?([:AM,:PM])end #((param == :AM) or (param == :PM)) end
  def hour24?(param) param.int? and param.in?(0...DAY_IN_HOUR) end
  def hour12?(param) param.int? and param.in?(1..(HALF_DAY_IN_HOUR)) end
  def min?(param) param.int? and param.in?(0...HOUR_IN_MIN) end
  def sec?(param) param.int? and param.in?(0...MIN_IN_SEC) end
  def day_sec?(param) param.int? and param.in?(0...DAY_IN_SEC) end
  
 def clock?(param) param.clock12? or param.clock24? or param.clock_sec? end

  
def normalize(seconds)
  seconds % DAY_IN_SEC
end
  
  #ClockSec als Klasse
#ClockSec ::=  ClockSec[:clock_sec] :: DaySec ::
#0 <= DaySec <= DAY_IN_SEC

def_class(:ClockSec,[:day_sec]) {
 
  def invariant?()
  day_sec?(day_sec)end  
    }
   
#Clock24 als Klasse
#Clock24 ::=  Clock24[:hour24, :min, :sec] :: hour24, min, sec ::
#0 <= hour24 <= DAY_IN_HOUR,
#0 <= min <= HOUR_IN_MIN,
#0 <= sec <= MIN_IN_SEC

def_class(:Clock24,[:hour24, :min, :sec]) {
 
  def invariant?()
    hour24?(hour24) and
    min?(min) and
    sec?(sec)
  end 
    }

#Clock12 als Klasse
#Clock12 ::= Clock12[:halve, :hour12, :min, :sec] :: halve, hour, min, sec ::
#halve = (:AM or :PM),
#0 <= hour12 <= (HALF_DAY_IN_HOUR),
#0 <= min <= HOUR_IN_MIN,
#0 <= sec <= MIN_IN_SEC

def_class(:Clock12,[:halve, :hour12, :min, :sec]) {
  def invariant?()
    halve?(halve) and
    hour12?(hour12) and
    min?(min) and
    sec?(sec)
  end
}
#Addieren von zwei Uhrzeiten in sekunden
#clock_sec_add ::sec1, sec2 :: ClockSec[day_sec] x ClockSec[day_sec] => ClockSec[Nat]
#where (sec1 and sec2) >= 0 and (sec1 + sec2) is in (0...DAY_IN_SEC)::
#(test (clock_sec_add(ClockSec[20], ClockSec[50]) => 70,
#clock_sec_add(ClockSec[3000], ClockSec[5600]) => 8600,
#clock_sec_add(ClockSec[0], ClockSec[0]) => 0,
#clock_sec_add(ClockSec[30], ClockSec["40"]) => Err,
#clock_sec_add(ClockSec["30"], ClockSec[40]) => Err,
#clock_sec_add(ClockSec[-10], ClockSec[0]) => Err,
#clock_sec_add(ClockSec[0], ClockSec[-10]) => Err
#clock_sec_add(ClockSec[-10]) => Err)

def clock_sec_add(sec1, sec2)
  check_pre((
      sec1.clock_sec? and
      sec2.clock_sec?
    ))
 
  sec = sec1.day_sec + sec2.day_sec
 
  ClockSec[normalize(sec)]

end

#Subtrahieren von zwei Uhrzeiten in sekunden
#clock_sec_add ::= sec1 - sec2 ::  ClockSec[day_sec] x ClockSec[day_sec] => ClockSec[Nat]
# where (day_sec1 and day_sec) >= 0
#(test (clock_sec_sub(ClockSec[90], ClockSec[20] => 70,
#clock_sec_add(ClockSec[5000], ClockSec[2000]) => 3000,
#clock_sec_add(ClockSec[0], ClockSec[0]) => 0,
#clock_sec_add(ClockSec[10], ClockSec[20]) => ClockSec[86390],
#clock_sec_add(ClockSec[30], ClockSec["40"]) => Err,
#clock_sec_add(ClockSec["30"], ClockSec[40]) => Err,
#clock_sec_add(ClockSec[[-10], ClockSec[0]) => Err,
#clock_sec_add(ClockSec[0], ClockSec[-10]) => Err,
#
#clock_sec_add(ClockSec[-10]) => Err)

def clock_sec_sub(sec1, sec2)
  check_pre((
      sec1.clock_sec? and
      sec2.clock_sec?
    ))
 sec = sec1.day_sec - sec2.day_sec
 
  ClockSec[normalize(sec)]
end

#nachfolger einer uhrzeit, angegeben in sekunden
#clock_sec_succ ::= sec1  ::  ClockSec => ClockSec ::
#(test (clock_sec_succ(ClockSec[90] => ClockSec[91],
#clock_sec_succ(ClockSec[5000]) => 5001,
#clock_sec_succ(ClockSec[86399]) => 0,
#clock_sec_succClockSec[0]) => 1,
#clock_sec_succ(ClockSec["40"]) => Err,
#clock_sec_succ(ClockSec[-10]) => Err,)

def clock_sec_succ(sec1)
  check_pre((sec1.clock_sec?))
 
  clock_sec_add(sec1, ClockSec[1])
end

#vorgänger einer uhrzeit, angegeben in sekunden
#clock_sec_pred ::= sec1  ::  ClockSec[day_sec] => ClockSec[Nat]
# where (sec1 ) >= 0 ::
#(test (clock_sec_pred(ClockSec[90] => 89,
#clock_sec_pred(ClockSec[5000]) => 4999,
#clock_sec_pred(ClockSec[1]) => 0,
#clock_sec_pred(ClockSec[0]) => 86399,
#clock_sec_pred(ClockSec["40"]) => Err,
#clock_sec_pred(ClockSec[-10]) => Err,)

def clock_sec_pred(sec1)
  check_pre((sec1.clock_sec?))
 
 clock_sec_sub(sec1, ClockSec[1])
end

#Clock24 auf ClockSec konvertieren
#clock24_to_clocksec ::= clock :: Clock24[hour24, min, sec] => ClockSec[day_sec] ::
#test(clock_24_to_clocksec(Clock24[0, 0, 0]) => ClockSec[0],
#clock_24_to_clocksec(Clock24[10, 10, 10]) => ClockSec[36610],
#clock_24_to_clocksec(Clock24[0, 0, "a"]) => Err,
#clock_24_to_clocksec(Clock24[0, "a", 0]) => Err
#clock_24_to_clocksec(Clock24["a", 0, 0]) => Err
#clock_24_to_clocksec(Clock24[0, 0, -1]) => Err
#clock_24_to_clocksec(Clock24[0, -1, 0]) => Err
#clock_24_to_clocksec(Clock24[-1, 0, 0]) => Err)

def clock24_to_clocksec(clock)
  check_pre((clock.clock24?))
    ClockSec[(clock.hour24 * HOUR_IN_SEC) + (clock.min * MIN_IN_SEC) + clock.sec]
    
end

#Clock12 auf ClockSec konvertieren
#clock12_to_clocksec ::= clock :: Clock12[halve, hour12, min, sec] => ClockSec[day_sec] ::
#test
#(clock_12_to_clocksec(Clock12[:AM, 12, 0, 0]) => ClockSec[0], 
#clock_12_to_clocksec(Clock12[:PM, 12, 0, 0]) => ClockSec[43200],
#clock_12_to_clocksec(Clock12[:AM, 10, 10, 10]) => ClockSec[36610],
#clock_12_to_clocksec(Clock12[0, 0, "a"]) => Err,
#clock_12_to_clocksec(Clock12[0, "a", 0]) => Err
#clock_12_to_clocksec(Clock12["a", 0, 0]) => Err
#clock_12_to_clocksec(Clock12[0, 0, -1]) => Err
#clock_12_to_clocksec(Clock12[0, -1, 0]) => Err
#clock_12_to_clocksec(Clock12[-1, 0, 0]) => Err)

def clock12_to_clocksec(clock)
  check_pre((clock.clock12?))
  
   sec = (((clock.halve == :AM ? 0 : 12) * HOUR_IN_SEC) +
      ((clock.hour12 == 12) ? 0 : (clock.hour12 * HOUR_IN_SEC)) + 
      (clock.min * MIN_IN_SEC) + clock.sec)
    ClockSec[normalize(sec)]
end

#ClockSec zu Clock24 konvertieren
#clocksec_to_clock24  ::= clock :: Clocksec[day_sec] -> Clock24[hour24, min, sec] ::
#test(clocksec_to_clock24(ClockSec[43200]) => Clock24[12, 0, 0],
#clocksec_to_clock24(ClockSec[47593] => Clock24[13, 13, 13],
#clocksec_to_clock24(ClockSec["a"]) => Err,
#clocksec_to_clock24("a") => Err)

def clocksec_to_clock24(clock)
   check_pre((clock.clock_sec?))
   
  #schreibarbeit ersparen, clock.day_sec = param
  
  hrs_min_sec_from_secs(clock.day_sec)
  
   Clock24[hrs_min_sec_from_secs(clock.day_sec)[0],hrs_min_sec_from_secs(clock.day_sec)[1],hrs_min_sec_from_secs(clock.day_sec)[2]]
end

#ClockSec zu Clock12 konvertieren
#clocksec_to_clock12  ::= clock :: Clocksec[day_sec] -> Clock12[halve, hour12, min, sec] ::
#test(clocksec_to_clock12(ClockSec[43200])) => Clock12[:AM,12, 0, 0],
#clocksec_to_clock12(ClockSec[47593]) => Clock12[:PM, 1, 13, 13],
#clocksec_to_clock12(ClockSec["a"]) => Err,
#clocksec_to_clock12("a") => Err


#def clocksec_to_clock12(clock)
#  
#  check_pre((clock.clock_sec?))
#  
#  if clock.day_sec == 0 then Clock12[:AM,12,0,0]
#  else
#    hour = clock.day_sec.divmod(HOUR_IN_SEC)[0]
#    min = (clock.day_sec.divmod(HOUR_IN_SEC)[1]).divmod(MIN_IN_SEC)[0]
#    sec = (clock.day_sec.divmod(HOUR_IN_SEC)[1]).divmod(MIN_IN_SEC)[1]
#    
#    
#    if hour > 11 then
#      hour = hour - (HALF_DAY_IN_HOUR)
#      (hour == 0 ? hour = 12 : hour)
#      halve = :PM
#    else
#      (hour == 0 ? hour = 12 : hour)
#      halve = :AM
#    end
#    
#  Clock12[halve, hour, min, sec]
#  end
#  
#end


def clocksec_to_clock12(clock)
  
  check_pre((clock.clock_sec?))
  
  

  halve = (clock.day_sec > HALF_DAY_IN_SEC) ? :PM : :AM
  
  seconds = halve == :AM ? clock.day_sec : clock.day_sec % HALF_DAY_IN_SEC
 
  Clock12[halve,hrs_min_sec_from_secs(seconds)[0] == 0 ? HALF_DAY_IN_HOUR : hrs_min_sec_from_secs(seconds)[0],hrs_min_sec_from_secs(seconds)[1],hrs_min_sec_from_secs(seconds)[2]]
end


def hrs_min_sec_from_secs(seconds)
  hour = seconds.divmod(HOUR_IN_SEC)[0]
  min = (seconds.divmod(HOUR_IN_SEC)[1]).divmod(MIN_IN_SEC)[0]
  sec = (seconds.divmod(HOUR_IN_SEC)[1]).divmod(MIN_IN_SEC)[1]
  [hour, min, sec]
end



#Clock24 zu Clock12 konvertieren
#clock24_to_clock12 ::= clock :: Clock24[hour24, min, sec] -> Clock12[halve, hour12, min, sec] ::
#test (clock24_to_clock12(clock24[11,11,11])) => Clock12[:AM,11,11,11],
#(clock24_to_clock12(Clock24[13,13,13])) => Clock12[:PM,1,13,13],
#(clock24_to_clock12(Clock24[0,11,11])) => Clock12[:AM,12,11,11],
#(clock24_to_clock12(Clock24[12,11,11])) => Clock12[:PM,12,11,11],
#(clock24_to_clock12(Clock24["a",1,1]) => Err,
#(clock24_to_clock12(Clock24[1,"1"a",1]) => Err,
#(clock24_to_clock12(Clock24[1,1,""a"]) => Err,
#(clock24_to_clock12(Clock24[-1,1,1]) => Err,
#(clock24_to_clock12(Clock24[1,-1,1]) => Err,
#(clock24_to_clock12(Clock24[1,1,-1]) => Err,

def clock24_to_clock12(clock)
  check_pre((clock.clock24?))
  
clocksec_to_clock12(clock24_to_clocksec(clock))
end


#Clock12 zu Clock24 konvertieren
#clock12_to_clock24 ::= clock :: Clock12[halve, hour12, min, sec] -> Clock24[hour24, min, sec] ::
#test (clock12_to_clock24(Clock12[:AM,11,11,11]) => Clock24[11,11,11]),
#(clock12_to_clock24(Clock12[:PM,1,13,13]) => Clock24[13,13,13],
#(clock12_to_clock24(Clock12[:AM,12,11,11])) => Clock24[0,11,11],
#(clock12_to_clock24(Clock12[:PM,12,11,11])) => Clock24[12,11,11],
#(clock12_to_clock24(Clock12["a",1,1,1]) => Err,
#(clock12_to_clock24(Clock12[:AM,"a",1,1]) => Err,
#(clock12_to_clock24(Clock12[:AM,1,"1"a",1]) => Err,
#(clock12_to_clock24(Clock12[:AM,1,1,""a"]) => Err,
#(clock24_to_clock12(Clock12[-1,1,1,1]) => Err,
#(clock24_to_clock12(Clock12[:AM,-1,1,1]) => Err,
#(clock24_to_clock12(Clock12[:AM,1,-1,1]) => Err,
#(clock24_to_clock12(Clock12[:AM,1,1,-1]) => Err)

def clock12_to_clock24(clock)
  check_pre((clock.clock12?))

  clocksec_to_clock24(clock12_to_clocksec(clock))
end

#to_clocksec 
#Konvertierung in eine Sekundenuhr
#to_clocksec ::= clock :: Clock24[hour24, min, sec] or Clock12[halve, hour12, min, sec] or ClockSec[day_sec] -> 
#ClockSec[day_sec]
#test(to_clocksec(Clock12[:AM, 12, 0, 0]) => ClockSec[0], 
#to_clocksec(Clock12[:PM, 1, 13, 13]) => ClockSec[47593],
#to_clocksec(Clock24[0, 0, 0]) => ClockSec[0],
#to_clocksec(Clock24[10, 10, 10]) => ClockSec[36610],
#to_clocksec(ClockSec[3000] => ClockSec[3000],
#to_clocksec(200) => Err,
#to_clocksec("a") => Err)

def to_clocksec(clock)
  check_pre((clock?(clock)))
  if clock.clock24? then clock24_to_clocksec(clock)
  elsif clock.clock12? then clock12_to_clocksec(clock)
  else clock
  end
end

#to_clock24
#Konvertierung in eine 24 stunden-Uhr
#to_clock24 ::= clock :: Clock12 or ClockSec 
#-> Clock24[hour24, min, sec]
#test (to_clock24(ClockSec[43200]) => Clock24[12, 0, 0],
#to_clock24(ClockSec[47593] => Clock24[13, 13, 13], 
#(to_clock24(Clock12[:AM,11,11,11]) => Clock24[11,11,11]),
#(to_clock24(Clock12[:PM,1,13,13]) => Clock24[13,13,13],
#to_clock24(200) => Err,
#to_clock24("a") => Err

def to_clock24(clock)
  check_pre((clock?(clock)))
  
  if clock.clock12? then clock12_to_clock24(clock)
  elsif clock.clock_sec? then clocksec_to_clock24(clock)
  else clock
  end
  
end

#to_clock12
#Konvertierung in eine 12 stunden uhr
#to_clock12 ::= clock :: Clock24[hour24, min, sec] or ClockSec[day_sec]
#-> Clock12[halve, hour12, min, sec]
#test(to_clock12((ClockSec[43200])) => Clock12[:AM,12, 0, 0],
#(to_clock12(ClockSec[47593])) => Clock12[:PM, 1, 13, 13],
#(to_clock12(clock24[11,11,11])) => Clock12[:AM,11,11,11],
#(to_clock12(Clock24[13,13,13])) => Clock12[:PM,1,13,13],
#to_clock24(200) => Err,
#to_clock24("a") => Err

def to_clock12(clock)
  check_pre((clock?(clock)))
  
  if clock.clock24? then clock24_to_clock12(clock)
  elsif clock.clock_sec? then clocksec_to_clock12(clock)
  else clock
  end
end

#to_clock
#beliebige konversion von uhren
#to_clock ::= clock1, clock2 :: Clock x Clock -> Clock ::
#test(to_clock(Clock24[6,6,6], ClockSec[43200]) => Clock24[12,0,0],
#to_clock(Clock24[12,3,1], Clock12[:PM,12,0,0]) => Clock24[12,0,0],
#to_clock(ClockSec[10000], Clock12[:AM, 12,12,12]) => ClockSec[732],
#to_clock(ClockSec[10000], Clock24[12,0,0]) => ClockSec[43200],
#to_clock(Clock12[:PM, 1,1,1], clock24[0,0,0]) => Clock12[:AM, 12,0,0]
#to_clock(Clock12[:PM,1,1,1], clocksec[0]) => Clock12[:AM, 12,0,0]
#to_clock(Clock12[:AM, 12,0,0], 200) => Err,
#to_clock("a". Clock12[:AM, 12,0,0]) => Err)

def to_clock(clock1, clock2)
  check_pre(( clock?(clock1) and (clock?(clock2)) ))

  if    clock1.clock12? then to_clock12(clock2)
  elsif clock1.clock24? then to_clock24(clock2)
  else                       to_clocksec(clock2)
  end
end
  
  #clock_add
  #Addieren von zwei Uhrzeiten
  #clock_add ::= clock1, clock2 :: Clock x Clock => Clock ::
  #test(clock_add(ClockSec[3000], ClockSec[5600])) => ClockSec[8600]
  #(clock_add(Clocksec[3000], Clock24[1,1,1])) => ClockSec[6661]
  #(clock_add(Clocksec[3000], Clock12[:AM,1,1,1])) => ClockSec[6661]
  #(clock_add(Clock12[:AM,1,1,1], ClockSec[1000])) => Clock12[:AM,1,17,41]
  #(clock_add(Clock12[:AM,1,1,1], Clock12[:AM,1,1,1])) => Clock12[:AM,2,2,2]
  #(clock_add(Clock12[:AM,1,1,1], Clock24[1,1,1])) => Clock12[:AM,2,2,2]
  #(clock_add(Clock24[1,1,1], ClockSec[1000])) => Clock24[1,17,17]
  #(clock_add(Clock24[1,1,1], Clock12[:AM,1,1,1])) => Clock24[2,2,2]
  #(clock_add(Clock24[1,1,1], Clock24[1,1,1])) => Clock24[2,2,2]
  #exc
  #clock_add(ClockSec["a], ClockSec[5600])) => Err
  #clock_add(ClockSec[3000], ClockSec["a"])) => Err
  #clock_add(ClockSec[-1], ClockSec[5600])) => Err
  #clock_add(ClockSec[3000], ClockSec[-1])) => Err
  #(clock_add(Clocksec["a"], Clock24[1,1,1])) => Err
  #(clock_add(Clocksec[3000], Clock24["a",1,1])) => Err
  #(clock_add(Clocksec[3000], Clock24[1,"a",1])) => Err
  #(clock_add(Clocksec[3000], Clock24[1,1,"a"])) => Err
  #(clock_add(Clocksec[-1], Clock24[1,1,1])) => Err
  #(clock_add(Clocksec[3000], Clock24[-1,1,1])) => Err
  #(clock_add(Clocksec[3000], Clock24[1,-1,1])) => Err
  #(clock_add(Clocksec[3000], Clock24[1,1,-1])) => Err
  #(clock_add(Clocksec["a"], Clock12[:AM,1,1,1])) => Err
  #(clock_add(Clocksec[3000], Clock12["a",1,1,1])) => Err
  #(clock_add(Clocksec[3000], Clock12[:AM,"a",1,1])) => Err
  #(clock_add(Clocksec[3000], Clock12[:AM,1,"a",1])) => Err
  #(clock_add(Clocksec[3000], Clock12[:AM,1,1,"a"])) => Err
  #(clock_add(Clocksec[-1], Clock12[:AM,1,1,1])) => Err
  #(clock_add(Clocksec[3000], Clock12[:AM,-1,1,1])) => Err
  #(clock_add(Clocksec[3000], Clock12[:AM,1,-1,1])) => Err
  #(clock_add(Clocksec[3000], Clock12[:AM,1,1,-1])) => Err
  #(clock_add(Clock12["a",1,1,1], ClockSec[1000])) => Err
  #(clock_add(Clock12[:AM,"a",1,1], ClockSec[1000])) => Err
  #(clock_add(Clock12[:AM,1,"a",1], ClockSec[1000])) => Err
  #(clock_add(Clock12[:AM,1,1,"a"], ClockSec[1000])) => Err
  #(clock_add(Clock12[:AM,1,1,1], ClockSec["a"])) => Err
  #(clock_add(Clock12[:AM,-1,1,1], ClockSec[1000])) => Err
  #(clock_add(Clock12[:AM,1,-1,1], ClockSec[1000])) => Err
  #(clock_add(Clock12[:AM,1,1,-1], ClockSec[1000])) => Err
  #(clock_add(Clock12[:AM,1,1,1], ClockSec[-1])) => Err
  #(clock_add(Clock12["a",1,1,1], Clock12[:AM,1,1,1])) => Err
  #(clock_add(Clock12[:AM,"a",1,1], Clock12[:AM,1,1,1])) => Err
  #(clock_add(Clock12[:AM,1,"a",1], Clock12[:AM,1,1,1])) => Err
  #(clock_add(Clock12[:AM,1,1,"a"], Clock12[:AM,1,1,1])) => Err
  #(clock_add(Clock12[:AM,1,1,1], Clock12["a",1,1,1])) => Err
  #(clock_add(Clock12[:AM,1,1,1], Clock12[:AM,"a",1,1])) => Err
  #(clock_add(Clock12[:AM,1,1,1], Clock12[:AM,1,"a",1])) => Err
  #(clock_add(Clock12[:AM,1,1,1], Clock12[:AM,1,1,"a"])) => Err
  #(clock_add(Clock12[:AM,-1,1,1], Clock12[:AM,1,1,1])) => Err
  #(clock_add(Clock12[:AM,1,-1,1], Clock12[:AM,1,1,1])) => Err
  #(clock_add(Clock12[:AM,1,1,-1], Clock12[:AM,1,1,1])) => Err
  #(clock_add(Clock12[:AM,1,1,1], Clock12[:AM,-1,1,1])) => Err
  #(clock_add(Clock12[:AM,1,1,1], Clock12[:AM,1,-1,1])) => Err
  #(clock_add(Clock12[:AM,1,1,1], Clock12[:AM,1,1,-1])) => Err
  #(clock_add(Clock12["a",1,1,1], Clock24[1,1,1])) => Err
  #(clock_add(Clock12[:AM,"a",1,1], Clock24[1,1,1])) => Err
  #(clock_add(Clock12[:AM,1,"a",1], Clock24[1,1,1])) => Err
  #(clock_add(Clock12[:AM,1,1,"a"], Clock24[1,1,1])) => Err
  #(clock_add(Clock12[:AM,1,1,1], Clock24["a",1,1])) => Err
  #(clock_add(Clock12[:AM,1,1,1], Clock24[1,"a",1])) => Err
  #(clock_add(Clock12[:AM,1,1,1], Clock24[1,1,"a"])) => Err
  #(clock_add(Clock12[:AM,-1,1,1], Clock24[1,1,1])) => Err
  #(clock_add(Clock12[:AM,1,-1,1], Clock24[1,1,1])) => Err
  #(clock_add(Clock12[:AM,1,1,-1], Clock24[1,1,1])) => Err
  #(clock_add(Clock12[:AM,1,1,1], Clock24[-1,1,1])) => Err
  #(clock_add(Clock12[:AM,1,1,1], Clock24[1,-1,1])) => Err
  #(clock_add(Clock12[:AM,1,1,1], Clock24[1,1,-1])) => Err
  #(clock_add(Clock24["a",1,1], ClockSec[1000])) => Err
  #(clock_add(Clock24[1,"a",1], ClockSec[1000])) => Err
  #(clock_add(Clock24[1,1,"a"], ClockSec[1000])) => Err
  #(clock_add(Clock24[1,1,1], ClockSec["a"])) => Err
  #(clock_add(Clock24[-1,1,1], ClockSec[1000])) => Err
  #(clock_add(Clock24[1,-1,1], ClockSec[1000])) => Err
  #(clock_add(Clock24[1,1,-1], ClockSec[1000])) => Err
  #(clock_add(Clock24[1,1,1], ClockSec[-1000])) => Err
  #(clock_add(Clock24["a",1,1], Clock12[:AM,1,1,1])) => Err
  #(clock_add(Clock24[1,"a",1], Clock12[:AM,1,1,1])) => Err
  #(clock_add(Clock24[1,1,"a"], Clock12[:AM,1,1,1])) => Err
  #(clock_add(Clock24[1,1,1], Clock12["a",1,1,1])) => Err
  #(clock_add(Clock24[1,1,1], Clock12[:AM,"a",1,1])) => Err
  #(clock_add(Clock24[1,1,1], Clock12[:AM,1,"a",1])) => Err
  #(clock_add(Clock24[1,1,1], Clock12[:AM,1,1,"a"])) => Err
  #(clock_add(Clock24[-1,1,1], Clock12[:AM,1,1,1])) => Err
  #(clock_add(Clock24[1,-1,1], Clock12[:AM,1,1,1])) => Err
  #(clock_add(Clock24[1,1,-1], Clock12[:AM,1,1,1])) => Err
  #(clock_add(Clock24[1,1,1], Clock12[:AM,-1,1,1])) => Err
  #(clock_add(Clock24[1,1,1], Clock12[:AM,1,-1,1])) => Err
  #(clock_add(Clock24[1,1,1], Clock12[:AM,1,1,-1])) => Err
  #(clock_add(Clock24["a",1,1], Clock24[1,1,1])) => Err
  #(clock_add(Clock24[1,"a",1], Clock24[1,1,1])) => Err
  #(clock_add(Clock24[1,1,"a"], Clock24[1,1,1])) => Err
  #(clock_add(Clock24[1,1,1], Clock24["a",1,1])) => Err
  #(clock_add(Clock24[1,1,1], Clock24[1,"a",1])) => Err
  #(clock_add(Clock24[1,1,1], Clock24[1,1,"a"])) => Err
  #(clock_add(Clock24[-1,1,1], Clock24[1,1,1])) => Err
  #(clock_add(Clock24[1,-1,1], Clock24[1,1,1])) => Err
  #(clock_add(Clock24[1,1,-1], Clock24[1,1,1])) => Err
  #(clock_add(Clock24[1,1,1], Clock24[-1,1,1])) => Err
  #(clock_add(Clock24[1,1,1], Clock24[1,-1,1])) => Err
  #(clock_add(Clock24[1,1,1], Clock24[1,1,-1])) => Err
  
  def clock_add(clock1, clock2)
     check_pre(( clock?(clock1) and (clock?(clock2)) ))

    to_clock(clock1, (clock_sec_add(to_clocksec(clock1), to_clocksec(clock2))))
  end
  
  #clock_sub
  #Subtrahieren von zwei Uhrzeiten
  #clock_sub ::= clock1, clock2 :: Clock x Clock => Clock ::
  #test(clock_sub(ClockSec[83800], ClockSec[5600])) => ClockSec[8600]
  #(clock_sub(Clocksec[85739], Clock24[1,1,1])) => ClockSec[6661]
  #(clock_sub(Clocksec[85739], Clock12[:AM,1,1,1])) => ClockSec[6661]
  #(clock_sub(Clock12[:AM,1,1,1], ClockSec[1000])) => Clock12[:PM,12,44,45]
  #(clock_sub(Clock12[:AM,1,1,1], Clock12[:AM,1,1,1])) => Clock12[:AM,12,0,0]
  #(clock_sub(Clock12[:AM,1,1,1], Clock24[1,1,1])) => Clock12[:AM,12,0,0]
  #(clock_sub(Clock24[1,1,1], ClockSec[1000])) => Clock24[0,44,45]
  #(clock_sub(Clock24[1,1,1], Clock12[:AM,1,1,1])) => Clock24[2,2,2]
  #(clock_sub(Clock24[1,1,1], Clock24[1,1,1])) => Clock24[2,2,2]
  #exc
  #clock_sub(ClockSec["a"], ClockSec[5600])) => Err
  #clock_sub(ClockSec[3000], ClockSec["a"])) => Err
  #clock_sub(ClockSec[-1], ClockSec[5600])) => Err
  #clock_sub(ClockSec[3000], ClockSec[-1])) => Err
  #(clock_sub(Clocksec["a"], Clock24[1,1,1])) => Err
  #(clock_sub(Clocksec[3000], Clock24["a",1,1])) => Err
  #(clock_sub(Clocksec[3000], Clock24[1,"a",1])) => Err
  #(clock_sub(Clocksec[3000], Clock24[1,1,"a"])) => Err
  #(clock_sub(Clocksec[-1], Clock24[1,1,1])) => Err
  #(clock_sub(Clocksec[3000], Clock24[-1,1,1])) => Err
  #(clock_sub(Clocksec[3000], Clock24[1,-1,1])) => Err
  #(clock_sub(Clocksec[3000], Clock24[1,1,-1])) => Err
  #(clock_sub(Clocksec["a"], Clock12[:AM,1,1,1])) => Err
  #(clock_sub(Clocksec[3000], Clock12["a",1,1,1])) => Err
  #(clock_sub(Clocksec[3000], Clock12[:AM,"a",1,1])) => Err
  #(clock_sub(Clocksec[3000], Clock12[:AM,1,"a",1])) => Err
  #(clock_sub(Clocksec[3000], Clock12[:AM,1,1,"a"])) => Err
  #(clock_sub(Clocksec[-1], Clock12[:AM,1,1,1])) => Err
  #(clock_sub(Clocksec[3000], Clock12[:AM,-1,1,1])) => Err
  #(clock_sub(Clocksec[3000], Clock12[:AM,1,-1,1])) => Err
  #(clock_sub(Clocksec[3000], Clock12[:AM,1,1,-1])) => Err
  #(clock_sub(Clock12["a",1,1,1], ClockSec[1000])) => Err
  #(clock_sub(Clock12[:AM,"a",1,1], ClockSec[1000])) => Err
  #(clock_sub(Clock12[:AM,1,"a",1], ClockSec[1000])) => Err
  #(clock_sub(Clock12[:AM,1,1,"a"], ClockSec[1000])) => Err
  #(clock_sub(Clock12[:AM,1,1,1], ClockSec["a"])) => Err
  #(clock_sub(Clock12[:AM,-1,1,1], ClockSec[1000])) => Err
  #(clock_sub(Clock12[:AM,1,-1,1], ClockSec[1000])) => Err
  #(clock_sub(Clock12[:AM,1,1,-1], ClockSec[1000])) => Err
  #(clock_sub(Clock12[:AM,1,1,1], ClockSec[-1])) => Err
  #(clock_sub(Clock12["a",1,1,1], Clock12[:AM,1,1,1])) => Err
  #(clock_sub(Clock12[:AM,"a",1,1], Clock12[:AM,1,1,1])) => Err
  #(clock_sub(Clock12[:AM,1,"a",1], Clock12[:AM,1,1,1])) => Err
  #(clock_sub(Clock12[:AM,1,1,"a"], Clock12[:AM,1,1,1])) => Err
  #(clock_sub(Clock12[:AM,1,1,1], Clock12["a",1,1,1])) => Err
  #(clock_sub(Clock12[:AM,1,1,1], Clock12[:AM,"a",1,1])) => Err
  #(clock_sub(Clock12[:AM,1,1,1], Clock12[:AM,1,"a",1])) => Err
  #(clock_sub(Clock12[:AM,1,1,1], Clock12[:AM,1,1,"a"])) => Err
  #(clock_sub(Clock12[:AM,-1,1,1], Clock12[:AM,1,1,1])) => Err
  #(clock_sub(Clock12[:AM,1,-1,1], Clock12[:AM,1,1,1])) => Err
  #(clock_sub(Clock12[:AM,1,1,-1], Clock12[:AM,1,1,1])) => Err
  #(clock_sub(Clock12[:AM,1,1,1], Clock12[:AM,-1,1,1])) => Err
  #(clock_sub(Clock12[:AM,1,1,1], Clock12[:AM,1,-1,1])) => Err
  #(clock_sub(Clock12[:AM,1,1,1], Clock12[:AM,1,1,-1])) => Err
  #(clock_sub(Clock12["a",1,1,1], Clock24[1,1,1])) => Err
  #(clock_sub(Clock12[:AM,"a",1,1], Clock24[1,1,1])) => Err
  #(clock_sub(Clock12[:AM,1,"a",1], Clock24[1,1,1])) => Err
  #(clock_sub(Clock12[:AM,1,1,"a"], Clock24[1,1,1])) => Err
  #(clock_sub(Clock12[:AM,1,1,1], Clock24["a",1,1])) => Err
  #(clock_sub(Clock12[:AM,1,1,1], Clock24[1,"a",1])) => Err
  #(clock_sub(Clock12[:AM,1,1,1], Clock24[1,1,"a"])) => Err
  #(clock_sub(Clock12[:AM,-1,1,1], Clock24[1,1,1])) => Err
  #(clock_sub(Clock12[:AM,1,-1,1], Clock24[1,1,1])) => Err
  #(clock_sub(Clock12[:AM,1,1,-1], Clock24[1,1,1])) => Err
  #(clock_sub(Clock12[:AM,1,1,1], Clock24[-1,1,1])) => Err
  #(clock_sub(Clock12[:AM,1,1,1], Clock24[1,-1,1])) => Err
  #(clock_sub(Clock12[:AM,1,1,1], Clock24[1,1,-1])) => Err
  #(clock_sub(Clock24["a",1,1], ClockSec[1000])) => Err
  #(clock_sub(Clock24[1,"a",1], ClockSec[1000])) => Err
  #(clock_sub(Clock24[1,1,"a"], ClockSec[1000])) => Err
  #(clock_sub(Clock24[1,1,1], ClockSec["a"])) => Err
  #(clock_sub(Clock24[-1,1,1], ClockSec[1000])) => Err
  #(clock_sub(Clock24[1,-1,1], ClockSec[1000])) => Err
  #(clock_sub(Clock24[1,1,-1], ClockSec[1000])) => Err
  #(clock_sub(Clock24[1,1,1], ClockSec[-1000])) => Err
  #(clock_sub(Clock24["a",1,1], Clock12[:AM,1,1,1])) => Err
  #(clock_sub(Clock24[1,"a",1], Clock12[:AM,1,1,1])) => Err
  #(clock_sub(Clock24[1,1,"a"], Clock12[:AM,1,1,1])) => Err
  #(clock_sub(Clock24[1,1,1], Clock12["a",1,1,1])) => Err
  #(clock_sub(Clock24[1,1,1], Clock12[:AM,"a",1,1])) => Err
  #(clock_sub(Clock24[1,1,1], Clock12[:AM,1,"a",1])) => Err
  #(clock_sub(Clock24[1,1,1], Clock12[:AM,1,1,"a"])) => Err
  #(clock_sub(Clock24[-1,1,1], Clock12[:AM,1,1,1])) => Err
  #(clock_sub(Clock24[1,-1,1], Clock12[:AM,1,1,1])) => Err
  #(clock_sub(Clock24[1,1,-1], Clock12[:AM,1,1,1])) => Err
  #(clock_sub(Clock24[1,1,1], Clock12[:AM,-1,1,1])) => Err
  #(clock_sub(Clock24[1,1,1], Clock12[:AM,1,-1,1])) => Err
  #(clock_sub(Clock24[1,1,1], Clock12[:AM,1,1,-1])) => Err
  #(clock_sub(Clock24["a",1,1], Clock24[1,1,1])) => Err
  #(clock_sub(Clock24[1,"a",1], Clock24[1,1,1])) => Err
  #(clock_sub(Clock24[1,1,"a"], Clock24[1,1,1])) => Err
  #(clock_sub(Clock24[1,1,1], Clock24["a",1,1])) => Err
  #(clock_sub(Clock24[1,1,1], Clock24[1,"a",1])) => Err
  #(clock_sub(Clock24[1,1,1], Clock24[1,1,"a"])) => Err
  #(clock_sub(Clock24[-1,1,1], Clock24[1,1,1])) => Err
  #(clock_sub(Clock24[1,-1,1], Clock24[1,1,1])) => Err
  #(clock_sub(Clock24[1,1,-1], Clock24[1,1,1])) => Err
  #(clock_sub(Clock24[1,1,1], Clock24[-1,1,1])) => Err
  #(clock_sub(Clock24[1,1,1], Clock24[1,-1,1])) => Err
  #(clock_sub(Clock24[1,1,1], Clock24[1,1,-1])) => Err
  
  def clock_sub(clock1,clock2)
     check_pre(( clock?(clock1) and (clock?(clock2)) ))

    to_clock(clock1, (clock_sec_sub(to_clocksec(clock1), to_clocksec(clock2))))
  end
  
  
  #clock_succ
  #Nachfolger einer Uhrzeit
  #clock_succ ::= clock1,clock2 :: Clock x Clock => Clock :: 
  #test(clock_succ(ClockSec[1], ClockSec[1]) => Clock24[2]
  #(clock_succ(ClockSec[1], Clock12[:AM,1,1,1]) => ClockSec[3662]
  #(clock_succ(ClockSec[1], Clock24[1,1,1] => [3662]
  #(clock_succ(Clock12[:AM,1,1,1], ClockSec[1]) => Clock12[:AM,1,1,2]
  #(clock_succ(Clock12[:AM,1,1,1], Clock12[:AM,1,1,1]) => Clock12[:AM,1,1,2]
  #(clock_succ(Clock12[:AM,1,1,1], Clock24[1,1,1] => Clock12[:AM,1,1,2]
  #(clock_succ(Clock24[1,1,1], ClockSec[1]) => Clock24[1,1,2]
  #(clock_succ(Clock24[1,1,1]), Clock12[:AM,1,1,1] => Clock24[1,1,2]
  #(clock_succ(Clock24[1,1,1], Clock24[1,1,1]) => Clock24[1,1,2]
  #exc
  #clock_succ(ClockSec["a"], ClockSec[5600])) => Err
  #clock_succ(ClockSec[3000], ClockSec["a"])) => Err
  #clock_succ(ClockSec[-1], ClockSec[5600])) => Err
  #clock_succ(ClockSec[3000], ClockSec[-1])) => Err
  #(clock_succ(Clocksec["a"], Clock24[1,1,1])) => Err
  #(clock_succ(Clocksec[3000], Clock24["a",1,1])) => Err
  #(clock_succ(Clocksec[3000], Clock24[1,"a",1])) => Err
  #(clock_succ(Clocksec[3000], Clock24[1,1,"a"])) => Err
  #(clock_succ(Clocksec[-1], Clock24[1,1,1])) => Err
  #(clock_succ(Clocksec[3000], Clock24[-1,1,1])) => Err
  #(clock_succ(Clocksec[3000], Clock24[1,-1,1])) => Err
  #(clock_succ(Clocksec[3000], Clock24[1,1,-1])) => Err
  #(clock_succ(Clocksec["a"], Clock12[:AM,1,1,1])) => Err
  #(clock_succ(Clocksec[3000], Clock12["a",1,1,1])) => Err
  #(clock_succ(Clocksec[3000], Clock12[:AM,"a",1,1])) => Err
  #(clock_succ(Clocksec[3000], Clock12[:AM,1,"a",1])) => Err
  #(clock_succ(Clocksec[3000], Clock12[:AM,1,1,"a"])) => Err
  #(clock_succ(Clocksec[-1], Clock12[:AM,1,1,1])) => Err
  #(clock_succ(Clocksec[3000], Clock12[:AM,-1,1,1])) => Err
  #(clock_succ(Clocksec[3000], Clock12[:AM,1,-1,1])) => Err
  #(clock_succ(Clocksec[3000], Clock12[:AM,1,1,-1])) => Err
  #(clock_succ(Clock12["a",1,1,1], ClockSec[1000])) => Err
  #(clock_succ(Clock12[:AM,"a",1,1], ClockSec[1000])) => Err
  #(clock_succ(Clock12[:AM,1,"a",1], ClockSec[1000])) => Err
  #(clock_succ(Clock12[:AM,1,1,"a"], ClockSec[1000])) => Err
  #(clock_succ(Clock12[:AM,1,1,1], ClockSec["a"])) => Err
  #(clock_succ(Clock12[:AM,-1,1,1], ClockSec[1000])) => Err
  #(clock_succ(Clock12[:AM,1,-1,1], ClockSec[1000])) => Err
  #(clock_succ(Clock12[:AM,1,1,-1], ClockSec[1000])) => Err
  #(clock_succ(Clock12[:AM,1,1,1], ClockSec[-1])) => Err
  #(clock_succ(Clock12["a",1,1,1], Clock12[:AM,1,1,1])) => Err
  #(clock_succ(Clock12[:AM,"a",1,1], Clock12[:AM,1,1,1])) => Err
  #(clock_succ(Clock12[:AM,1,"a",1], Clock12[:AM,1,1,1])) => Err
  #(clock_succ(Clock12[:AM,1,1,"a"], Clock12[:AM,1,1,1])) => Err
  #(clock_succ(Clock12[:AM,1,1,1], Clock12["a",1,1,1])) => Err
  #(clock_succ(Clock12[:AM,1,1,1], Clock12[:AM,"a",1,1])) => Err
  #(clock_succ(Clock12[:AM,1,1,1], Clock12[:AM,1,"a",1])) => Err
  #(clock_succ(Clock12[:AM,1,1,1], Clock12[:AM,1,1,"a"])) => Err
  #(clock_succ(Clock12[:AM,-1,1,1], Clock12[:AM,1,1,1])) => Err
  #(clock_succ(Clock12[:AM,1,-1,1], Clock12[:AM,1,1,1])) => Err
  #(clock_succ(Clock12[:AM,1,1,-1], Clock12[:AM,1,1,1])) => Err
  #(clock_succ(Clock12[:AM,1,1,1], Clock12[:AM,-1,1,1])) => Err
  #(clock_succ(Clock12[:AM,1,1,1], Clock12[:AM,1,-1,1])) => Err
  #(clock_succ(Clock12[:AM,1,1,1], Clock12[:AM,1,1,-1])) => Err
  #(clock_succ(Clock12["a",1,1,1], Clock24[1,1,1])) => Err
  #(clock_succ(Clock12[:AM,"a",1,1], Clock24[1,1,1])) => Err
  #(clock_succ(Clock12[:AM,1,"a",1], Clock24[1,1,1])) => Err
  #(clock_succ(Clock12[:AM,1,1,"a"], Clock24[1,1,1])) => Err
  #(clock_succ(Clock12[:AM,1,1,1], Clock24["a",1,1])) => Err
  #(clock_succ(Clock12[:AM,1,1,1], Clock24[1,"a",1])) => Err
  #(clock_succ(Clock12[:AM,1,1,1], Clock24[1,1,"a"])) => Err
  #(clock_succ(Clock12[:AM,-1,1,1], Clock24[1,1,1])) => Err
  #(clock_succ(Clock12[:AM,1,-1,1], Clock24[1,1,1])) => Err
  #(clock_succ(Clock12[:AM,1,1,-1], Clock24[1,1,1])) => Err
  #(clock_succ(Clock12[:AM,1,1,1], Clock24[-1,1,1])) => Err
  #(clock_succ(Clock12[:AM,1,1,1], Clock24[1,-1,1])) => Err
  #(clock_succ(Clock12[:AM,1,1,1], Clock24[1,1,-1])) => Err
  #(clock_succ(Clock24["a",1,1], ClockSec[1000])) => Err
  #(clock_succ(Clock24[1,"a",1], ClockSec[1000])) => Err
  #(clock_succ(Clock24[1,1,"a"], ClockSec[1000])) => Err
  #(clock_succ(Clock24[1,1,1], ClockSec["a"])) => Err
  #(clock_succ(Clock24[-1,1,1], ClockSec[1000])) => Err
  #(clock_succ(Clock24[1,-1,1], ClockSec[1000])) => Err
  #(clock_succ(Clock24[1,1,-1], ClockSec[1000])) => Err
  #(clock_succ(Clock24[1,1,1], ClockSec[-1000])) => Err
  #(clock_succ(Clock24["a",1,1], Clock12[:AM,1,1,1])) => Err
  #(clock_succ(Clock24[1,"a",1], Clock12[:AM,1,1,1])) => Err
  #(clock_succ(Clock24[1,1,"a"], Clock12[:AM,1,1,1])) => Err
  #(clock_succ(Clock24[1,1,1], Clock12["a",1,1,1])) => Err
  #(clock_succ(Clock24[1,1,1], Clock12[:AM,"a",1,1])) => Err
  #(clock_succ(Clock24[1,1,1], Clock12[:AM,1,"a",1])) => Err
  #(clock_succ(Clock24[1,1,1], Clock12[:AM,1,1,"a"])) => Err
  #(clock_succ(Clock24[-1,1,1], Clock12[:AM,1,1,1])) => Err
  #(clock_succ(Clock24[1,-1,1], Clock12[:AM,1,1,1])) => Err
  #(clock_succ(Clock24[1,1,-1], Clock12[:AM,1,1,1])) => Err
  #(clock_succ(Clock24[1,1,1], Clock12[:AM,-1,1,1])) => Err
  #(clock_succ(Clock24[1,1,1], Clock12[:AM,1,-1,1])) => Err
  #(clock_succ(Clock24[1,1,1], Clock12[:AM,1,1,-1])) => Err
  #(clock_succ(Clock24["a",1,1], Clock24[1,1,1])) => Err
  #(clock_succ(Clock24[1,"a",1], Clock24[1,1,1])) => Err
  #(clock_succ(Clock24[1,1,"a"], Clock24[1,1,1])) => Err
  #(clock_succ(Clock24[1,1,1], Clock24["a",1,1])) => Err
  #(clock_succ(Clock24[1,1,1], Clock24[1,"a",1])) => Err
  #(clock_succ(Clock24[1,1,1], Clock24[1,1,"a"])) => Err
  #(clock_succ(Clock24[-1,1,1], Clock24[1,1,1])) => Err
  #(clock_succ(Clock24[1,-1,1], Clock24[1,1,1])) => Err
  #(clock_succ(Clock24[1,1,-1], Clock24[1,1,1])) => Err
  #(clock_succ(Clock24[1,1,1], Clock24[-1,1,1])) => Err
  #(clock_succ(Clock24[1,1,1], Clock24[1,-1,1])) => Err
  #(clock_succ(Clock24[1,1,1], Clock24[1,1,-1])) => Err
  
  def clock_succ(clock1,clock2)
     check_pre(( clock?(clock1) and (clock?(clock2)) ))
    
  to_clock(clock1, (clock_sec_succ(to_clocksec(clock2))))
  end
  
  #clock_pred
  #Vorgänger einer Uhrzeit
  #clock_pred ::= clock1,clock2 :: Clock x Clock => Clock :: 
  #test(clock_pred(ClockSec[2], ClockSec[1]) => Clock24[0]
  #(clock_pred(ClockSec[1], Clock12[:AM,1,1,1]) => ClockSec[3660]
  #(clock_pred(ClockSec[1], Clock24[1,1,1] => [3660]
  #(clock_pred(Clock12[:AM,1,1,1], ClockSec[1]) => Clock12[:AM,1,1,0]
  #(clock_pred(Clock12[:AM,1,1,1], Clock12[:AM,1,1,1]) => Clock12[:AM,1,1,0]
  #(clock_pred(Clock12[:AM,1,1,1], Clock24[1,1,1] => Clock12[:AM,1,1,0]
  #(clock_pred(Clock24[1,1,1], ClockSec[1]) => Clock24[1,1,0]
  #(clock_pred(Clock24[1,1,1]), Clock12[:AM,1,1,1] => Clock24[1,1,0]
  #(clock_pred(Clock24[1,1,1], Clock24[1,1,1]) => Clock24[1,1,0]
  #exc
  #clock_pred(ClockSec["a"], ClockSec[5600])) => Err
  #clock_pred(ClockSec[3000], ClockSec["a"])) => Err
  #clock_pred(ClockSec[-1], ClockSec[5600])) => Err
  #clock_pred(ClockSec[3000], ClockSec[-1])) => Err
  #(clock_pred(Clocksec["a"], Clock24[1,1,1])) => Err
  #(clock_pred(Clocksec[3000], Clock24["a",1,1])) => Err
  #(clock_pred(Clocksec[3000], Clock24[1,"a",1])) => Err
  #(clock_pred(Clocksec[3000], Clock24[1,1,"a"])) => Err
  #(clock_pred(Clocksec[-1], Clock24[1,1,1])) => Err
  #(clock_pred(Clocksec[3000], Clock24[-1,1,1])) => Err
  #(clock_pred(Clocksec[3000], Clock24[1,-1,1])) => Err
  #(clock_pred(Clocksec[3000], Clock24[1,1,-1])) => Err
  #(clock_pred(Clocksec["a"], Clock12[:AM,1,1,1])) => Err
  #(clock_pred(Clocksec[3000], Clock12["a",1,1,1])) => Err
  #(clock_pred(Clocksec[3000], Clock12[:AM,"a",1,1])) => Err
  #(clock_pred(Clocksec[3000], Clock12[:AM,1,"a",1])) => Err
  #(clock_pred(Clocksec[3000], Clock12[:AM,1,1,"a"])) => Err
  #(clock_pred(Clocksec[-1], Clock12[:AM,1,1,1])) => Err
  #(clock_pred(Clocksec[3000], Clock12[:AM,-1,1,1])) => Err
  #(clock_pred(Clocksec[3000], Clock12[:AM,1,-1,1])) => Err
  #(clock_pred(Clocksec[3000], Clock12[:AM,1,1,-1])) => Err
  #(clock_pred(Clock12["a",1,1,1], ClockSec[1000])) => Err
  #(clock_pred(Clock12[:AM,"a",1,1], ClockSec[1000])) => Err
  #(clock_pred(Clock12[:AM,1,"a",1], ClockSec[1000])) => Err
  #(clock_pred(Clock12[:AM,1,1,"a"], ClockSec[1000])) => Err
  #(clock_pred(Clock12[:AM,1,1,1], ClockSec["a"])) => Err
  #(clock_pred(Clock12[:AM,-1,1,1], ClockSec[1000])) => Err
  #(clock_pred(Clock12[:AM,1,-1,1], ClockSec[1000])) => Err
  #(clock_pred(Clock12[:AM,1,1,-1], ClockSec[1000])) => Err
  #(clock_pred(Clock12[:AM,1,1,1], ClockSec[-1])) => Err
  #(clock_pred(Clock12["a",1,1,1], Clock12[:AM,1,1,1])) => Err
  #(clock_pred(Clock12[:AM,"a",1,1], Clock12[:AM,1,1,1])) => Err
  #(clock_pred(Clock12[:AM,1,"a",1], Clock12[:AM,1,1,1])) => Err
  #(clock_pred(Clock12[:AM,1,1,"a"], Clock12[:AM,1,1,1])) => Err
  #(clock_pred(Clock12[:AM,1,1,1], Clock12["a",1,1,1])) => Err
  #(clock_pred(Clock12[:AM,1,1,1], Clock12[:AM,"a",1,1])) => Err
  #(clock_pred(Clock12[:AM,1,1,1], Clock12[:AM,1,"a",1])) => Err
  #(clock_pred(Clock12[:AM,1,1,1], Clock12[:AM,1,1,"a"])) => Err
  #(clock_pred(Clock12[:AM,-1,1,1], Clock12[:AM,1,1,1])) => Err
  #(clock_pred(Clock12[:AM,1,-1,1], Clock12[:AM,1,1,1])) => Err
  #(clock_pred(Clock12[:AM,1,1,-1], Clock12[:AM,1,1,1])) => Err
  #(clock_pred(Clock12[:AM,1,1,1], Clock12[:AM,-1,1,1])) => Err
  #(clock_pred(Clock12[:AM,1,1,1], Clock12[:AM,1,-1,1])) => Err
  #(clock_pred(Clock12[:AM,1,1,1], Clock12[:AM,1,1,-1])) => Err
  #(clock_pred(Clock12["a",1,1,1], Clock24[1,1,1])) => Err
  #(clock_pred(Clock12[:AM,"a",1,1], Clock24[1,1,1])) => Err
  #(clock_pred(Clock12[:AM,1,"a",1], Clock24[1,1,1])) => Err
  #(clock_pred(Clock12[:AM,1,1,"a"], Clock24[1,1,1])) => Err
  #(clock_pred(Clock12[:AM,1,1,1], Clock24["a",1,1])) => Err
  #(clock_pred(Clock12[:AM,1,1,1], Clock24[1,"a",1])) => Err
  #(clock_pred(Clock12[:AM,1,1,1], Clock24[1,1,"a"])) => Err
  #(clock_pred(Clock12[:AM,-1,1,1], Clock24[1,1,1])) => Err
  #(clock_pred(Clock12[:AM,1,-1,1], Clock24[1,1,1])) => Err
  #(clock_pred(Clock12[:AM,1,1,-1], Clock24[1,1,1])) => Err
  #(clock_pred(Clock12[:AM,1,1,1], Clock24[-1,1,1])) => Err
  #(clock_pred(Clock12[:AM,1,1,1], Clock24[1,-1,1])) => Err
  #(clock_pred(Clock12[:AM,1,1,1], Clock24[1,1,-1])) => Err
  #(clock_pred(Clock24["a",1,1], ClockSec[1000])) => Err
  #(clock_pred(Clock24[1,"a",1], ClockSec[1000])) => Err
  #(clock_pred(Clock24[1,1,"a"], ClockSec[1000])) => Err
  #(clock_pred(Clock24[1,1,1], ClockSec["a"])) => Err
  #(clock_pred(Clock24[-1,1,1], ClockSec[1000])) => Err
  #(clock_pred(Clock24[1,-1,1], ClockSec[1000])) => Err
  #(clock_pred(Clock24[1,1,-1], ClockSec[1000])) => Err
  #(clock_pred(Clock24[1,1,1], ClockSec[-1000])) => Err
  #(clock_pred(Clock24["a",1,1], Clock12[:AM,1,1,1])) => Err
  #(clock_pred(Clock24[1,"a",1], Clock12[:AM,1,1,1])) => Err
  #(clock_pred(Clock24[1,1,"a"], Clock12[:AM,1,1,1])) => Err
  #(clock_pred(Clock24[1,1,1], Clock12["a",1,1,1])) => Err
  #(clock_pred(Clock24[1,1,1], Clock12[:AM,"a",1,1])) => Err
  #(clock_pred(Clock24[1,1,1], Clock12[:AM,1,"a",1])) => Err
  #(clock_pred(Clock24[1,1,1], Clock12[:AM,1,1,"a"])) => Err
  #(clock_pred(Clock24[-1,1,1], Clock12[:AM,1,1,1])) => Err
  #(clock_pred(Clock24[1,-1,1], Clock12[:AM,1,1,1])) => Err
  #(clock_pred(Clock24[1,1,-1], Clock12[:AM,1,1,1])) => Err
  #(clock_pred(Clock24[1,1,1], Clock12[:AM,-1,1,1])) => Err
  #(clock_pred(Clock24[1,1,1], Clock12[:AM,1,-1,1])) => Err
  #(clock_pred(Clock24[1,1,1], Clock12[:AM,1,1,-1])) => Err
  #(clock_pred(Clock24["a",1,1], Clock24[1,1,1])) => Err
  #(clock_pred(Clock24[1,"a",1], Clock24[1,1,1])) => Err
  #(clock_pred(Clock24[1,1,"a"], Clock24[1,1,1])) => Err
  #(clock_pred(Clock24[1,1,1], Clock24["a",1,1])) => Err
  #(clock_pred(Clock24[1,1,1], Clock24[1,"a",1])) => Err
  #(clock_pred(Clock24[1,1,1], Clock24[1,1,"a"])) => Err
  #(clock_pred(Clock24[-1,1,1], Clock24[1,1,1])) => Err
  #(clock_pred(Clock24[1,-1,1], Clock24[1,1,1])) => Err
  #(clock_pred(Clock24[1,1,-1], Clock24[1,1,1])) => Err
  #(clock_pred(Clock24[1,1,1], Clock24[-1,1,1])) => Err
  #(clock_pred(Clock24[1,1,1], Clock24[1,-1,1])) => Err
  #(clock_pred(Clock24[1,1,1], Clock24[1,1,-1])) => Err
  
  def clock_pred(clock1,clock2)
     check_pre(( clock?(clock1) and (clock?(clock2)) ))
    
  to_clock(clock1, (clock_sec_pred(to_clocksec(clock2))))
  end
  
  #allgemeine selektoren
  
  #clock_sec ::= clock :: Clock12[halve, hour12, min, sec] or Clock24[hour24, min,sec] ClockSec[day_sec]::
  # clock -> Int :: (test (clock_sec(Clock12[:AM,1,1,1] => 1,
  #clock_sec(Clock24[1,1,1]) => 1, clock_sec(ClockSec[3661]) => 1
  #clock_sec(3) => Err, clock_sec("a") => Err)
  
  def clock_sec(clock)
    check_pre(( clock?(clock)))
    
    (to_clock24(clock)).sec
  end
  
    #clock_hour24 ::= clock :: Clock12[halve, hour12, min, sec] or Clock24[hour24, min,sec] ClockSec[day_sec]::
  # clock -> Int :: (test (clock_hour24(Clock12[:AM,1,1,1] => 1,
  #clock_hour24(Clock24[1,1,1]) => 1, clock_hour24(ClockSec[3661]) => 1
  #clock_hour24(3) => Err, clock_hour24("a") => Err)
  
    def clock_hour24(clock)
    check_pre(( clock?(clock)))
    to_clock24(clock).hour24
    end
  
  #clock_hour12 ::= clock :: Clock12[halve, hour12, min, sec] or Clock24[hour24, min,sec] ClockSec[day_sec]::
  # clock -> Int :: (test (clock_hour12(Clock12[:AM,1,1,1] => 1,
  #clock_hour12(Clock24[1,1,1]) => 1, clock_hour12(ClockSec[3661]) => 1
  #clock_hour12(3) => Err, clock_hour12("a") => Err)
  
      def clock_hour12(clock)
    check_pre(( clock?(clock)))
    to_clock12(clock).hour12
  end
  
      
  #clock_min ::= clock :: Clock12[halve, hour12, min, sec] or Clock24[hour24, min,sec] ClockSec[day_sec]::
  # clock -> Int :: (test (clock_min(Clock12[:AM,1,1,1] => 1,
  #clock_min(Clock24[1,1,1]) => 1, clock_min(ClockSec[3661]) => 1
  #clock_min(3) => Err, clock_min("a") => Err)
 
   def clock_min(clock)
    check_pre(( clock?(clock)))
    to_clock12(clock).min
  end
  
  #clock_halve ::= clock :: Clock12[halve, hour12, min, sec] or Clock24[hour24, min,sec] ClockSec[day_sec]::
  # clock -> :AM|:PM :: (test (clock_halve(Clock12[:AM,1,1,1] => :AM,
  #clock_halve(Clock24[1,1,1]) => :AM, clock_halve(ClockSec[3661]) => :AM
  #clock_halve(3) => Err, clock_halve("a") => Err)
  
      def clock_halve(clock)
    check_pre(( clock?(clock)))
    to_clock12(clock).halve
    
  end